$\forall$$A$:Type, $P$:($A$$\rightarrow$prop\{i:l\}). strong{-}subtype(\{$x$:$A$$\mid$ $P$($x$)\} ; $A$)